Inference at * 1 0 4 2 
Iof proof for Lemma eq int cases test:



1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. bb:. ((i = j) = bb)
8. P(if (i = j) then x else y fi )
9.   Type
10. (i = j)  
11. bb:. ((i = j) = bb)  Type
  P(if (i = j) then x else y fi ) 

latex

 by (\p.D (get_int_arg `i` p) p) 

latex

 1: 

 1: 7. bb : 
 1: 8. (i = j) = bb
 1: 9. P(if (i = j) then x else y fi )
 1: 10.   Type
 1: 11. (i = j)  
 1: 12. bb:. ((i = j) = bb)  Type
 1:   P(if (i = j) then x else y fi )
 .

Definitions

x:A. B(x), t  T, if b then t else f fi , f(a), (i = j), s = t, , , , x:AB(x), Type, x:A  B(x), x:A. B(x)